'xxx'1 =a1 'yyy'1 = false   

latex

Definitions	eq_atom$n(x;y), false
Lemmas	bfalse wf